T:Type, l:(T List), x:T. l_member!(x; l; T)  prop{i:l} 

latex

Definitions	False, A, A  B, P  Q, P  Q, A c B, x:A. B(x), l_member!(x; l; T), prop{i:l}, t  T, x:A. B(x),
Lemmas	select wf, length wf1, nat wf